<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-1"
 http-equiv="content-type">
  <title>ProofAssistantGUIQuickHOWTO</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
 alink="#000088" link="#0000ff" vlink="#ff0000">
<big><big><span style="font-weight: bold;">Proof Assistant GUI Quick
HOWTO<br>
<br>
</span></big></big><big><span style="font-weight: bold;">See also:<br>
</span></big><a href="PAUserGuide/Start.html">Proof Assistant User Guide</a><br>
<a href="ProofAssistantGUIDetailedInfo.html">ProofAssistantGUIDetailedInfo.html</a><br>
<a href="ProofAssistantGUIDeriveFeature.html">ProofAssistantGUIDeriveFeature.html</a><br>
<a href="StepUnifier.html">StepUnifier.html</a><br>
<a href="WorkVariables.html">WorkVariables.html</a><br>
<a href="../mmj2jar/PATutorial/PageLocalRef.mmp">PageLocalRef.mmp</a><br>
<a href="StepSelectorSearch.html">StepSelectorSearch.html</a><br>
<a href="UnifyEraseAndRederiveFormulasFeature.html">UnifyEraseAndRederiveFormulas.html</a><br>
<a href="BottomUpProving-ByNormMegill.html">BottomUpProving-ByNormMegill.html</a><br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;"></span></big><big><span
 style="font-weight: bold;">Purpose</span>:</big> <br>
<ul>
  <li>The main function of
the Proof Assistant GUI is to construct valid Metamath RPN-formatted
proofs. <br>
  </li>
  <li>Two distinct approaches to proof development are supported, and
these approaches can be combined. Top-Down proving derives a theorem's
conclusion by writing a sequence of proof
step formulas that logically lead to the conclusion, where each step is
justified by referencing an existing
Metamath assertion. Bottom-Up also builds a sequence of proof step
formulas, but it works backwards from the
conclusion, identifying in turn, the existing Metamath assertion which
justifies that each derivation step's formula. <br>
  </li>
  <li>mmj2 supports both Top-Down and Bottom-Up proving by providing
two important capabilities: 1) it uses a Unification Search algorithm
to find an existing assertion that justifies (unifies with) a proof
step and its formula; and 2) conversely, it provides a "Derive" feature
which generates proof step formulas when given the label (i.e. key) of
an existing assertion. <br>
  </li>
  <li>When a proof has been
successfully created, mmj2 generates a Metamath RPN-formatted proof
that can be exported or copied into a Metamath database.<br>
  </li>
</ul>
<br>
<span style="font-weight: bold;"><big>Motivations:</big> </span><br>
<ul>
  <li>One motivating idea behind the GUI is that it is difficult to
memorize
thousands of theorem and axiom statement labels, and it would be nice
to have a bit of help from the computer. A person may well be
capable of&nbsp; writing a series of formulas deriving the conclusion
of a theorem but have difficulty
recalling the Metamath statement labels justifying each step. The
primary Metamath database, set.mm, has nearly 10,000 statement labels!</li>
  <li>Another
motivation for the GUI is that metamath.exe's Proof Assistant
requires the user to enter proofs backwards, starting from the
conclusion and working towards the premises. The Proof Assistant GUI
allows the user to work forward or backward; that is, starting from the
hypotheses and deriving the conclusion, or the reverse. In fact, it is
possible to experiment using the GUI and create proof steps that head
off in a tangent without contributing to the conclusion :)</li>
</ul>
<br>
<big><span style="font-weight: bold;">Limitations:</span></big> <br>
<ul>
  <li><span style="text-decoration: underline;">The Proof Assistant GUI
does not update Metamath .mm files</span>.
A generated proof must either be manually pasted into the .mm file, or
"imported" into Metamath using the "eimmimp.cmd" which imports a mmj2
Proof Worksheet into a Metamath .mm database (see Metamath.com for more
information).<br>
  </li>
  <li>New
theorems, not already present in the Metamath files that are loaded,
can be proved, but new theorems not yet saved in the .mm file cannot
refer to each other. And, although $d can be added to a proof,&nbsp;
and both $d and $e specifications can be
coded with a new proof; <span style="text-decoration: underline;">all
variables, constants,&nbsp; variable
hypotheses and axioms referred to must already be present in the loaded
Metamath .mm file</span>.<br>
  </li>
</ul>
<br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;">Usage:</span></big><br>
<br>
Trigger/initiate/start the Run ProofAsstGUI using program BatchMMJ2 as
described elsewhere (for example, <a href="../mmj2jar/mmj2.bat">mmj2\mmj2jar\mmj2.bat</a>
). <br>
<br>
<span style="font-weight: bold; text-decoration: underline;">NOTE --
IMPORTANT: Run the mmj2.bat command from a Command Prompt window. The
Proof
Assistant GUI is triggered at the end of the regular BatchMMJ2 process
and if there are errors in the load, grammatical parse or RunParm
validation, error messages print out and the GUI does not appear. </span><br
 style="font-weight: bold; text-decoration: underline;">
<br>
When the GUI screen appears:<br>
<ul>
  <li>Select the <span style="font-weight: bold;">File/New Proof</span>
menu item<br>
  </li>
  <li>A dialogue box will appear asking "<span
 style="font-weight: bold;">Theorem label?</span>"</li>
  <li>Type in the label of a theorem in your .mm file and click "<span
 style="font-weight: bold;">OK</span>".</li>
  <li>A skeletal proof appears on the ProofAsstGUI main frame:</li>
</ul>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-family: monospace; font-weight: bold;">$( &lt;MM&gt;
&lt;PROOF_ASST&gt; THEOREM=a1i&nbsp; LOC_AFTER=?</span><br
 style="font-family: monospace; font-weight: bold;">
<br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">h1::a1i.1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ph </span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">2:?:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ?</span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">qed:?:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ( ps -&gt; ph ) </span><br
 style="font-family: monospace; font-weight: bold;">
<br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">$)</span></big><br>
<hr style="width: 100%; height: 2px;">The GUI frame is a free-form text
frame that is editable. (The contents of the text frame -- the text --
is called a "<span style="font-weight: bold;">Proof Worksheet</span>"
elsewhere in the mmj2 system, fyi.)&nbsp; Proof Step #2 above is a
skeleton proof step with
"<code style="font-weight: bold;">?</code>"s indicating the location of
fields to be entered. As shown below,
all we need to enter in Step #2 is a formula; there are no hypotheses
involved.<br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-family: monospace; font-weight: bold;">$( &lt;MM&gt;
&lt;PROOF_ASST&gt; THEOREM=a1i&nbsp; LOC_AFTER=?</span><br
 style="font-family: monospace; font-weight: bold;">
<br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">h1::a1i.1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ph </span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">2::&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ( ph -&gt; ( ps -&gt; ph ) ) </span><br
 style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">qed:1,2:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ( ps -&gt; ph ) </span><br
 style="font-family: monospace; font-weight: bold;">
<br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">$)</span></big><br>
<hr style="width: 100%; height: 2px;">Next select the <span
 style="font-weight: bold;">Unify/Unify (check proof)</span> menu item
or press the <code style="font-weight: bold;">Ctrl</code> and "<code
 style="font-weight: bold;">U</code>" keys simultaneously.<br>
<br>
The Proof Assistant performs validation and unification for each step
and generates "<span style="font-weight: bold;">Ref</span>" labels for
each properly unified step. And, if all
proof steps are correctly unified -- particularly especially the final,
"<code style="font-weight: bold;">qed</code>" step, the Metamath
RPN-format proof is also displayed:<br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-family: monospace; font-weight: bold;">$( &lt;MM&gt;
&lt;PROOF_ASST&gt; THEOREM=a1i&nbsp; LOC_AFTER=?</span><br
 style="font-family: monospace; font-weight: bold;">
<br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">h1::a1i.1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ph </span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">2::ax-1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ( ph -&gt; ( ps -&gt; ph ) ) </span><br
 style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">qed:1,2:ax-mp&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|- ( ps -&gt; ph ) <br>
<br>
<code>$=&nbsp;&nbsp;&nbsp; wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.</code><br>
<br>
</span><span style="font-family: monospace; font-weight: bold;">$)</span></big><br>
<hr style="width: 100%; height: 2px;">Voila! Proof complete. If
desired, save the Proof Assistant GUI text area to a file using the <span
 style="font-weight: bold;">File/SaveAs</span> menu item. And, if
desired, use the <span style="font-weight: bold;">Edit/Copy</span>
menu item to copy the Metamath RPN proof steps and then paste them into
to your .mm file.<br>
<br>
Now, for reference purposes, please compare the screen layout above to
this portion of the Metamath Proof Explorer html page for theorem a1i:<br>
<hr noshade="noshade" size="1">
<center>
<table summary="Proof of theorem" bgcolor="#eefffa" border="1"
 cellspacing="0">
  <caption><b>Proof of Theorem <font color="#006633">a1i</font></b></caption>
  <tbody>
    <tr>
      <th>Step</th>
      <th>Hyp</th>
      <th>Ref </th>
      <th>Expression</th>
    </tr>
    <tr align="left">
      <td>1</td>
      <td>&nbsp;</td>
      <td>a1i.1</td>
      <td><span class="i">. 2</span> <font color="#00cc00">&#8866; </font><font
 color="#0000ff"><i>&#966;</i></font></td>
    </tr>
    <tr align="left">
      <td>2</td>
      <td>&nbsp;</td>
      <td><a href="../../../metamath/althtml/ax-1.html">ax-1</a>&nbsp;<span
 class="r" style="color: rgb(255, 96, 96);">3</span></td>
      <td><span class="i">. 2</span> <font color="#00cc00">&#8866; </font>(<font
 color="#0000ff"><i>&#966;</i></font>
&#8594; (<font color="#0000ff"><i>&#968;</i></font> &#8594; <font color="#0000ff"><i>&#966;</i></font>))</td>
    </tr>
    <tr align="left">
      <td>3</td>
      <td>1, 2</td>
      <td><a href="../../../metamath/althtml/ax-mp.html">ax-mp</a>&nbsp;<span
 class="r" style="color: rgb(255, 96, 96);">6</span></td>
      <td><span class="i">1</span> <font color="#00cc00">&#8866; </font>(<font
 color="#0000ff"><i>&#968;</i></font>
&#8594; <font color="#0000ff"><i>&#966;</i></font>)</td>
    </tr>
  </tbody>
</table>
</center>
<font size="-1"><b></b></font>
<hr style="width: 100%; height: 2px;"><span style="font-weight: bold;">GENERAL
FACTOIDS about the GUI proof text area - AKA "Proof Worksheet":</span><br>
<ul>
  <li><span style="text-decoration: underline;">The Proof Assistant GUI
proof text area follows the format and rules of a single Metamath
comment statement</span>: it begins with "<code
 style="font-weight: bold;">$(</code>" and ends with "<code
 style="font-weight: bold;">$)</code>", <span
 style="font-style: italic;">must</span> consist of valid Metamath
tokens, and must <span style="font-style: italic;">not</span> contain
nested Metamath comments. (This is a
"feature" that allows the student/mathelogician to embed GUI proof
texts inside a Metamath
.mm file, if desired.)</li>
  <li>Any text entered prior to the <span style="font-weight: bold;">Header</span>'s
"<code><span style="font-weight: bold;">$(</span></code>" is treated as
an error. <br>
  </li>
  <li>Any text entered after the <span style="font-weight: bold;">Footer</span>'s
"<code style="font-weight: bold;">$)</code>" is ignored and will be
erased automatically.<br>
  </li>
  <li>Suggestion: use "<span style="font-weight: bold;">File/Save</span>"
frequently to avoid any mishaps.<br>
  </li>
  <li>There are six (6) types of proof text statements: <span
 style="font-weight: bold;">Header</span>, <span
 style="font-weight: bold;">Proof Step</span>, <span
 style="font-weight: bold;">Comment</span>, <span
 style="font-weight: bold;">Distinct Variables</span>, and <span
 style="font-weight: bold;">Generated Proof,</span> and <span
 style="font-weight: bold;">Footer</span> statements. (The <span
 style="font-weight: bold;">Generated Proof</span> statement is output
from by the Proof Assistant and is not (validly) enterable by the user.)<br>
  </li>
  <li><span style="text-decoration: underline; font-weight: bold;">Each
instance of one of these proof text statement types must begin in
column 1</span> of the GUI text area! <br>
  </li>
  <li style="text-decoration: underline; font-weight: bold;">A blank
character in column 1 of a line indicates continuation of the previous
statement.</li>
  <li>There
must be no extra text, no extraneous comments or remarks inside any of
the proof text statements. The Comment statement is the only
"authorized"
way to add commentary about a proof! (This rule makes the parser easier
to code.)<br>
  </li>
  <li><span style="text-decoration: underline;">The Proof Assistant GUI
program does not retain theorem-specific memory about the
user's interactions and progress towards a valid proof</span>
(note: as of Nov-1-2006, the program does retain a memory of the
sequence number/location of the current proof within the Metamath
database -- this information is used for browsing forward or backward,
but has no&nbsp; effect on processing the Proof Worksheet itself.) <span
 style="text-decoration: underline;">All relevant
proof information is contained in the Proof Text.</span> This means
that,
among other things, it is not necessary to begin a proof using the <span
 style="font-weight: bold;">File/New Proof</span> menu option. Proof
text can be entered elsewhere, say, with the text editor of your
choice, then be pasted (<span style="font-weight: bold;">Edit/Paste</span>)
into the GUI proof text area. Or, the File/Open menu option can be used
to load a file into the Proof Text area. Whatever is in the Proof Text
area can be validated/unified at any time using the <span
 style="font-weight: bold;">Unify/Unify (check proof)</span> menu
option. It is also possible --and allowed -- to change the <span
 style="font-weight: bold;">Header</span> statement's <code
 style="font-weight: bold;">THEOREM</code> and <code><span
 style="font-weight: bold;">LOC_AFTER</span></code> label values to
"clone" a proof.<br>
  </li>
  <li><span style="text-decoration: underline;">The Proof Assistant GUI
allows new theorems -- theorems not
already present in the loaded Metamath .mm file -- to be proved.</span>
The
design of the user interface requires that hypothesis proof step
"numbers" be prefixed with an "<code style="font-weight: bold;">h</code>",
and that the final proof step "number" equal "<code
 style="font-weight: bold;">qed</code>".
Given these bits of information, plus the <span
 style="font-weight: bold;">Header</span>'s <code
 style="font-weight: bold;">THEOREM=</code> label value and <code
 style="font-weight: bold;">LOC_AFTER=</code> value, plus any
(optional) <span style="font-weight: bold;">Distinct
Variable</span> statements, the Proof Assistant can construct a
Metamath theorem in memory
and then validate/unify its proof. The only limitation is that the GUI
does not provide a way to enter new dummy variable definitions as part
of the proof text; any variables referenced in a <span
 style="font-style: italic;">new theorem</span> proof must
be defined at the global scope level of the input Metamath .mm file.</li>
  <li>The <code style="font-weight: bold;">LOC_AFTER</code> field on
the proof text <span style="font-weight: bold;">Header</span>
statement is used only to specify the logical location of a new
theorem in the loaded set of Metamath statements; it is ignored when
present on a proof for an existing theorem. Location is significant in
Metamath because statements may refer only to previous statements in a
Metamath file. If <code style="font-weight: bold;">LOC_AFTER</code> is
left blank (or = "<code style="font-weight: bold;">?</code>"), then the
GUI treats the new theorem as if it were the last Metamath statement in
the database.<br>
  </li>
  <li>[Gedankenexperiment: do <code style="font-weight: bold;">File/New</code>
specifying "<code>a1i</code>". Then in the displayed proof text area,
change "<code style="font-weight: bold;">THEOREM=a1i</code>" in the <span
 style="font-weight: bold;">Header</span> statement to "<code
 style="font-weight: bold;">THEOREM=TESTa1i</code>", and set the <span
 style="font-weight: bold;">Step:Hyp<span
 style="font-family: monospace;">:</span><code></code>Ref</span> data
on the <code><span style="font-weight: bold;">qed</span></code> proof
step to "<code style="font-weight: bold;">qed:1</code>", but.do not
change "<code style="font-weight: bold;">LOC_AFTER=?</code>". Then
select menu item <span style="font-weight: bold;">Unify/Unify (check
proof)</span>. If the Proof Assistant GUI program is working correctly,
the unification algorithm will complete the proof, assigning <code
 style="font-weight: bold;">a1i</code> to the <code
 style="font-weight: bold;">qed</code> proof step <span
 style="font-weight: bold;">Ref</span>.]</li>
  <li>One or more <span style="font-weight: bold;">Distinct Variable</span>
statements, such as "<code style="font-weight: bold;">$d x y z</code>"
may be entered in the proof text area. <span
 style="text-decoration: underline;">Each must begin in column 1 of a
new, separate line of the proof text</span> (i.e. if two Distinct
Variable
statements are needed, then each must be entered on a separate proof
text area line.) This capability was added to the GUI specification as
an
afterthought because it was realized that figuring out the needed <code
 style="font-weight: bold;">$d</code>'s is an iterative process, with
some trial and error, even for highly expert Metamath users. <span
 style="text-decoration: underline;">A
Distinct Variable statement entered in a GUI proof text is treated as
an <span style="font-style: italic;">addition</span> of distinct
variable restrictions to those already present
for the theorem in the loaded Metamath .mm file</span> (except when
option "<code>GenerateNew</code>" is selected on the Edit/Set Soft Dj
Vars Error Handling menu item.). <br>
  </li>
</ul>
<br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;">Example of Proof Text area containing
Distinct Variables, Comments and free-form Formulas:</span></big><br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-family: monospace; font-weight: bold;">$( &lt;MM&gt;
&lt;PROOF_ASST&gt; THEOREM=a1i&nbsp; LOC_AFTER=?</span><br
 style="font-family: monospace; font-weight: bold;">
<br>
<code style="font-weight: bold;">* Comment begins with "*" in column 1
and <br>
&nbsp; continues until the next line of the Proof<br>
&nbsp; Text area which does not have a space in<br>
&nbsp; column 1.<br>
<br>
* Note how Formulas may be indented and spaced<br>
&nbsp; freely by the user, continuing onto as many<br>
&nbsp; lines as desired.<br>
&nbsp;&nbsp; </code><br
 style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">h1::a1i.1<br>
&nbsp;
|-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
ph </span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">2::<br>
&nbsp;
|-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
( ph <br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt; <br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
( ps -&gt; ph ) <br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
) </span><br style="font-family: monospace; font-weight: bold;">
<span style="font-family: monospace; font-weight: bold;">qed:1,2:<br>
&nbsp;
|-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
( ps -&gt; ph ) </span><br
 style="font-family: monospace; font-weight: bold;">
<br>
<code style="font-weight: bold;">* Following are Distinct Variable
statements<br>
&nbsp; (may occur anywhere inside the Proof Text<br>
&nbsp; between the Header and Footer statements):<br>
$d th ta<br>
$d ch ta<br>
<br>
* Note: Distinct Variable restrictions added<br>
&nbsp; are applied in conjunction with any Distinct<br>
&nbsp; Variable restrictions already contained in<br>
&nbsp; the Metamath .mm file for the Theorem unless<br>
&nbsp; "GenerateNew" is selected on the Edit/Set <br>
&nbsp; Soft Dj Vars Error Handling menu item.<br>
<br>
</code><span style="font-family: monospace; font-weight: bold;">$)</span></big><br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;">Tips on Effective Use (and programmer CYAs):</span></big><br>
<br>
<table style="text-align: left; width: 499px; height: 60px;" border="1"
 cellpadding="2" cellspacing="2">
  <tbody>
    <tr>
      <td style="vertical-align: top; width: 75px;"><span
 style="font-weight: bold;">Request<br>
Message<br>
Window<br>
      </span><span style="font-weight: bold;">Handling</span><br>
      </td>
      <td style="vertical-align: top;">Error and Informational messages
produced by the Proof Assistant GUI appear in a small text window
"pane" on the main Proof Assistant GUI window. A separate Request
Message window is created containing these messages and can be viewed
using Alt-Tab. <br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top; width: 75px;"><span
 style="font-weight: bold;">Unification</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Search</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Sequence</span><br>
      </td>
      <td style="vertical-align: top;">The program searches the loaded
Metamath assertions (from the .mm file(s)) in ascending database
sequence. That means that if two assertions satisfactorily unify with a
given proof step, the assertion that appears earliest in the input
files is used. If this is unacceptable the user can simply input the
correct assertion label.<br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Unify</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Search</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Exclusions</span><br>
      </td>
      <td style="vertical-align: top;">New RunParm to exclude loaded
assertions from the Unification search (example):<br>
      <br>
      <code><span style="font-weight: bold;">ProofAsstUnifySearchExclude,biigb,xxxid</span></code><br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Distinct</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Variable</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Errors and</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Alternative</span><br
 style="font-weight: bold;">
      <span style="font-weight: bold;">Unifications</span><br>
      </td>
      <td style="vertical-align: top;">When the user manually inputs a
Ref for a proof step and that Ref either does not unify satisfactorily
or has Distinct Variable restriction errors, a message is produced
showing the assertions that do unify with the proof step. In the case
where the user leaves the Ref blank and allows the program to search
for a unifying assertion, the first Ref that unifies with the proof
step is taken and used, provisionally. If the Ref has a Distinct
Variable restriction error, the search continues, looking for a perfect
unification without the $d errors; if this secondary search is
unsuccessful, an informational message displaying altervative
assertions is produced.<br>
      <br>
Note: The Edit menu (and input RunParm file) provide a choice about how
"soft" Distinct Variable restriction errors are handled. '"Soft" Dj
Vars Errors' refers to missing or incomplete $d statements on the
theorem being proved. The default setting is not to report these errors
but to "GenerateReplacements", which creates a complete set of $d
statements for the theorem being proved once unification is completed
for the 'qed' step of the proof. "Hard" errors, which occur when a pair
of substitution variables violates the $d restrictions specified by a
proof step Ref assertion are always reported and cannot be "fixed" by
the mmj2 program.<br>
      </td>
    </tr>
    <tr>
      <td style="vertical-align: top;"><span style="font-weight: bold;">Annotated<br>
RunParms<br>
.txt</span></td>
      <td style="vertical-align: top;">Many options to customize
processing can be set by updating the "RunParms.txt" file which is
input in the mmj2.bat command file. All RunParm values and options are
documented in <a href="../mmj2jar/AnnotatedRunParms.txt">mmj2\mmj2jar\AnnotatedRunParms.txt</a>.
For some features of mmj2, the AnnotatedRunParms.txt file is the only
source of documentation, so you may want to have a look; your
experience with the mmj2 Proof Assistant can be easily customized and
optimized to satisfy your personal requirements and preferences.<br>
      </td>
    </tr>
  </tbody>
</table>
<big><span style="font-weight: bold;"></span></big><br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;">See also:<br>
<br>
</span></big><a href="PAUserGuide/Start.html">Proof Assistant User Guide</a><br>
<a href="ProofAssistantGUIDetailedInfo.html">ProofAssistantGUIDetailedInfo.html</a><br>
<a href="ProofAssistantGUIDeriveFeature.html">ProofAssistantGUIDeriveFeature.html</a><br>
<hr style="width: 100%; height: 2px;"><big><span
 style="font-weight: bold;"><big></big></span></big><br>
</body>
</html>
